A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
(can-apply(f o g  ;x))  ((can-apply(g;x)) & (can-apply(f;do-apply(g;x)))) 

latex

ProofTree

Definitions	P & Q, {T}, P  Q, x:A. B(x), t  T, Type, x:AB(x), , Unit, left + right, ff, tt, do-apply(f;x), f(a), case b of inl(x) => s(x) | inr(y) => t(y), True, if b then t else f fi , b, , A c B, x:A  B(x), P  Q, P  Q, Top, False, A, s = t, can-apply(f;x), f o g
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, do-apply wf, btrue wf, bfalse wf, can-apply-compose